Taro Sekiyama

Abstract

Lung nodule classification is a class imbalanced problem, as nodules are found with much lower frequency than non-nodules. In the class imbalanced problem, conventional classifiers tend to be overwhelmed by the majority class and ignore the minority class. We showed that cascaded convolutional neural networks can classify the nodule candidates precisely for a class imbalanced nodule candidate data set in our previous study. In this paper, we propose Fusion classifier in conjunction with the cascaded convolutional neural network models. To fuse the models, nodule probabilities are calculated by using the convolutional neural network models at first. Then, Fusion classifier is trained and tested by the nodule probabilities. The proposed achieved the sensitivity of 94.4% and 95.9% at 4 and 8 false positives per scan in Free Receiver Operating Characteristics (FROC) curve analysis, respectively.

Abstract

We study an extension of typing graduala method to integrate dynamic typing and static typing smoothly in a language singleto parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically and dynamically typed languages, type safety, blame-subtyping theorem, and the guarantee gradualthe so-called refined criteria, advocated by Siek et al. We develop System FG, which is a gradually typed extension of System F with the dynamic type and a new type consistency relation, and translation to a new polymorphic blame calculus System FC, which is based on previous polymorphic blame calculi by Ahmed et al. The design of System FG and System FC, geared to the criteria, is influenced by the distinction between static and gradual type variables, first observed by Garcia and Cimini. This distinction is also useful to execute statically typed code without incurring additional overhead to manage type names as in the prior calculi. We prove that System FG satisfies most of the criteria: all but the hardest property of the gradual guarantee on semantics. We show that a key conjecture to prove the gradual guarantee leads to the Jack-of-All-Trades property, conjectured as an important property of the polymorphic blame calculus by Ahmed et al.

Abstract

Inspired by the recent evolution of deep neural networks (DNNs) in machine learning, we explore their application to PL-related topics. This paper is the first step towards this goal; we propose a proof-synthesis method for the negation-free propositional logic in which we use a DNN to obtain a guide of proof search. The idea is to view the proof-synthesis problem as a translation from a proposition to its proof. We train seq2seq, which is a popular network in neural machine translation, so that it generates a proof encoded as a Lung nodule classification is a class imbalanced problem @Comment-term of a given proposition. We implement the whole framework and empirically observe that a generated proof term is close to a correct proof in terms of the tree edit distance of AST. This observation justifies using the output from a trained seq2seq model as a guide for proof search.

Author-Izer

Abstract

Manifest contracts track precise program properties by refining types with predicates—e.g., x:Int|x > 0 denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give strong contracts to abstract types, precisely stating pre- and post-conditions while hiding implementation details—for example, an abstract type of stacks might specify that the pop operation has input type x:A Stack|not (empty x).

This article studies a polymorphic calculus with manifest contracts and establishes fundamental properties including type soundness and relational parametricity. Indeed, this is not the first work on polymorphic manifest contracts but existing calculi are not very satisfactory. Gronski et al. developed the Sage language, which introduces polymorphism through the Type:Type discipline, but they do not study parametricity. Some authors of this paper have produced two separate works: Belo, Greenberg, Igarashi, and Pierce (ESOP 2011) and Greenberg (PhD thesis) studied polymorphic manifest contracts and parametricity, but their calculi have metatheoretical problems in the type conversion relations—indeed, they depend on a few conjectures, which turn out to be false. Our calculus is the first polymorphic manifest calculus with parametricity, depending on no conjectures—it resolves the issues in prior calculi with delayed substitution on casts.

Author-Izer

Abstract

This paper studies hybrid contract verification for an imperative higher-order language based on a so-called manifest contract system. In manifest contract systems, contracts are part of static types and contract verification is hybrid in the sense that some contracts are statically verified, typically by subtyping, but others are dynamically by casts. It is, however, not trivial to extend existing manifest contract systems, which have been designed mostly for pure functional languages, to imperative features, mainly because of the lack of flow-sensitivity, which should be taken into account in verifying imperative programs statically.

We develop an imperative higher-order manifest contract system λH_ref for flow-sensitive hybrid contract verification. We introduce a computational variant of Nanevski et al's Hoare types, which are flow-sensitive types to represent pre- and postconditions of impure computation. Our Hoare types are computational in the sense that pre- and postconditions are given by Booleans in the same language as programs so that they are dynamically verifiable. λH_ref also supports refinement types as in existing manifest contract systems to describe flow-insensitive, state-independent contracts of pure computation. While it is desirable that any—possibly state-manipulating—predicate can be used in contracts, abuse of stateful operations will break the system. To control stateful operations in contracts, we introduce a region-based effect system, which allows contracts in refinement types and computational Hoare types to manipulate states, as long as they are observationally pure and read-only, respectively. We show that dynamic contract checking in our calculus is consistent with static typing in the sense that the final result obtained without dynamic contract violations satisfies contracts in its static type. It in particular means that the state after stateful computations satisfies their postconditions.

As in some of prior manifest contract systems, static contract verification in this work is “post facto,” that is, we first define our manifest contract system so that all contracts are checked at run time, formalize conditions when dynamic checks can be removed safely, and show that programs with and without such removable checks are contextually equivalent. We also apply the idea of post facto verification to region-based local reasoning, inspired by the frame rule of Separation Logic.

Abstract

Hidden units can play essential roles in modeling time-series having long-term dependency or on-linearity but make it difficult to learn associated parameters. Here we propose a way to learn such a time-series model by training a backward model for the time-reversed time-series, where the backward model has a common set of parameters as the original (forward) model. Our key observation is that only a subset of the parameters is hard to learn, and that subset is complementary between the forward model and the backward model. By training both of the two models, we can effectively learn the values of the parameters that are hard to learn if only either of the two models is trained. We apply bidirectional learning to a dynamic Boltzmann machine extended with hidden units. Numerical experiments with synthetic and real datasets clearly demonstrate advantages of bidirectional learning.

Abstract

Lung nodule classification is a class imbalanced problem because nodules are found in much lower frequency than non-nodules. In the class imbalanced problem, conventional classifiers tend to be overwhelmed by the majority class and ignore the minority class. We therefore propose cascaded convolutional neural networks to cope with the class imbalanced problem. In the proposed approach, multi-stage convolutional neural networks perform as single-sided classifiers to filter out obvious non-nodules. Successively, a convolutional neural network trained with a balanced data set calculates nodule probabilities. The proposed method achieved the sensitivity of 92.4% and 94.5% at 4 and 8 false positives per scan in Free Receiver Operating Characteristics (FROC) curve analysis, respectively.

Abstract

For development of reliable software, many verification methods have been studied so far. One of the most successful approaches is type systems, which have been tied to various kinds of programming languages from dynamically typed ones through dependently typed ones. Each of dynamic, static, and dependent typing has its own pros and cons and is not always sufficient for development of practical, reliable software. Our goal is to introduce a full-fledged programming language where dynamically, statically, and dependently typed code coexist and interact safely. In this thesis, we focus on three universal features in programming: delimited control, parametric polymorphism, and algebraic datatypes. These features are bases of current programming languages—delimited control provides control effects such as exception handling; polymorphism plays a key role in type-based abstraction and reuse of program components; algebraic datatypes are an usual tool to represent data structures. We study how these features are incorporated with mechanisms for integrating a certified and an uncertified worlds, based on gradual typing, which combines static and dynamic typing, and manifest contracts, which does static and dependent typing. We first study delimited control in integration of static and dynamic typing; this extension needs monitoring of capture and call of delimited continuations. We also investigate parametric polymorphism in a combination of static and dependent typing and show our extension is sound, in particular, parametricity does hold. Finally, an extension with algebraic datatypes lets us compare two major approaches to giving specifications to data structures from the point of view of computational efficiency. We believe that these extensions and insights obtained from them will contribute to achievement of our goal.

Author-Izer

Abstract

We study algebraic datatypes in a manifest contract system, a software contract system where contract information occurs as refinement types. We first compare two simple approaches: refinements on type constructors and refinements on data constructors. For example, lists of positive integers can be described by { l:int list | for_all (λy. y > 0) l } in the former, whereas by a user-defined datatype pos_list with cons of type {x:int | x > 0} ×pos_list →pos_list in the latter. The two approaches are complementary: the former makes it easier for a programmer to write types and the latter enables more efficient contract checking. To take the best of both worlds, we propose (1) a syntactic translation from refinements on type constructors to equivalent refinements on data constructors and (2) dynamically checked casts between different but compatible datatypes such as int list and pos_list. We define a manifest contract calculus to formalize the semantics of the casts and prove that the translation is correct.

Abstract

We study integration of static and dynamic typing in the presence of delimited-control operators. In a program where typed and untyped parts coexist, the run-time system has to monitor the flow of values between these parts and abort program execution if invalid values are passed. However, control operators, which enable us to implement useful control effects, make such monitoring tricky; in fact, it is known that, with a standard approach, certain communications between typed and untyped parts can be overlooked.

We propose a new cast-based mechanism to monitor all communications between typed and untyped parts for a language with control operators shift and reset. We extend a blame calculus with shift/reset to give its semantics (operational semantics and CPS transformation) and prove two important correctness properties of the proposed mechanism: Blame Theorem and soundness of the CPS transformation.

Abstract

A manifest contract calculus is a lambda-calculus with software contracts and dynamic contract checking, where software contracts are part of type information and dynamic contract checking is performed by casts from one type to another. Previous work for manifest contract calculi has studied an optimization to eliminate upcasts, and the correctness of the optimization by giving logical relations. However, all proofs of soundness of the logical relations w.r.t. contextual equivalence are incomplete.

We fix this unfortunate situation and even go further: we extend a polymorphic manifest contract calculus with a fixed-point operator, give logical relations for the extended calculus, and show their soundness with respect to what we call semi-typed contextual equivalence and that an upcast is logically related to an identity function.

概要

畳み込みニューラルネットワーク(CNN)は中間データを保存するためのメ モリ(ワークスペース)を割り当てることで高速化されることが知られ ている．本稿ではニューラルネットワーク(NN)を動的に構築・操作で きる深層学習フレームワークにおけるワークスペース管理手法を提案， CNNを自動的に高速化する．NNの動的構築によりNNが最低限必要とす るメモリ量を推定することが難しくなり，その結果ワークスペースに 割けるメモリ量の推測が困難になる．我々はNNが必要とするメモリを 空きメモリからだけではなくワークスペースからも割り当てることで ワークスペース割当を自動化しつつNNの構築を妨げない範囲でCNNを 高速化する．我々は提案手法をChainerに実装し，ワークスペースの 自動割当によりVGGNetなどの主要なCNNにおける伝搬処理が最大1.60 倍高速化されたことを確認した．

概要

顕在的契約計算は単純な型では捉えられないプログラムの性質—例えば 0での除算ができないといった制約—を表わしたソフトウェア契約を 型システムに取り入れた型付計算体系である．契約は篩(ふるい)型 (refinement type)として静的型情報に現われるが，成り立つことが 静的に保証できない契約はキャストにより実行時検査される．

本研究では代数的データ型を導入した顕在的契約計算を与え，その性質 について議論する．本研究で扱う代数的データ型は，構築子への契約 の付与や項変数の抽象化により，リストの昇順性のようなデータ構造 要素間の不変条件を型として表現できるだけでなく，構築子の対応関 係を明示した代数的データ型間のキャストにより不変条件の成立の可 否を実行時検査できる．また本論文ではデータ構造に関する実行時検 査の遅延化や計算体系の実装についても論ずる．

概要

顕在的契約計算体系は，実行時に検査されるソフトウェア契約の情報— 例えば，スタックの pop 操作は非空スタックを引数とする，といっ た，単純な型では捉えられない制約条件—が，篩(ふるい)型 (refinement type)として静的型情報に明示的に現れている型付計算 体系である．顕在的契約計算体系での実行時検査は型変換(キャスト) により実現される．

本研究では多相関数型と再帰関数を含む顕在的契約計算体系 F_H^fix において，部分型関係にある型の間のキャストであるアップキャスト が除去可能であることを，F_H^fix の弱型付文脈等価性とそれに対し 健全な論理関係を与え，アップキャストと恒等関数が論理関係にある ことを証明することで示す．